Computer programs and software are ubiquitous and are used not just to direct the functionality of conventional computers but also to control and enhance the functionality of a myriad of modern products and appliances. For instance, televisions, household appliances, cellular phones, automobiles, medical devices, and so forth, may incorporate computer programs which direct and enhance their functionality. The theoretical and practical analysis of computer programs is an important aspect of software research, development, modification, enhancement, and maintenance. The ability to analyze computer programs and reason about their execution, from both theoretical and practical perspectives, aids software developers by allowing them to make better and more informed choices during development of software and the modification or enhancement of existing software. Analysis of software is useful for proving correctness of code, for performing optimizations of existing code, for doing performance analysis and so on.
For purposes of analysis, it is often efficient and desirable to automate the reasoning about the complexity of software using tools and abstractions which can describe the properties and behavior of computer software. Computer software may often be formally described for the purposes of such analysis by specifying a set of constraints or axioms formalizing the relationships and operation of the software.
For a given set of constraints or axioms, it may be useful to reason about the implications of certain other constraints or imposed equalities within software systems. It is often desirable to reason about new constraints which are implied when equalities are imposed on a given set of initial or intermediate constraints and equalities. Formal theorem provers have been usefully employed in such reasoning and have proven to be very useful in a wide range of applications from computer software and hardware analysis, software systems requirements analysis, compiler verification. One type of prover, a Satisfiability Modulo Theories (SMT) solver, has been considered for such uses in hardware verification, analysis of algorithms, and verification of compiler correctness.
Satisfiability Modulo Theories (SMT) solvers, sometimes based upon a Davis-Putnam-Logemann-Loveland (DPLL) framework, have proven to be very useful for integrating theory reasoning for such purposes. A well known approach for incorporating quantifier reasoning with ground decision procedures has been used by the Simplify theorem prover described by Detlefs, Nelson, and Saxe. The Simplify theorem prover, for example, uses an E-matching algorithm that works against an E-graph to instantiate quantified variables. However, there are problems and limitations with the techniques and approaches employed thus far.
E-matching is known, in theory, to be NP-hard and the number of matches can be exponential in the size of the E-graph. It may be inefficient and it may consume large resources, both in time and space, to compute the matching on an E-graph to instantiate quantified variables which make up the terms and patterns of the systems being analyzed. The time and space resources necessary may grow exponentially with the number of patterns which need to be matched in a given situation. The practical overhead of using E-matching for quantifier instantiation, which is in many cases excessive, may be linked to the searching and maintaining sets of patterns that can efficiently retrieve new matches when E-graph operations introduce them.